<html>
<head><meta charset="utf-8"><title>sem-vs-syn-eq chalk#364 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html">sem-vs-syn-eq chalk#364</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="194328280"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194328280" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194328280">(Apr 16 2020 at 16:06)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> what's the right place to insert sem-syn lowering? My guess is "in <code>ClauseBuilder</code>'s <code>push_clause_with_priority</code>", am I right?</p>



<a name="194344928"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194344928" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194344928">(Apr 16 2020 at 18:08)</a>:</h4>
<p>Whats the difference between an <code>AliasTy</code> and a <code>TyData::Apply</code> with an <code>AssociatedType</code> name?</p>



<a name="194346536"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194346536" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194346536">(Apr 16 2020 at 18:20)</a>:</h4>
<p>The <code>TypeName::AssociatedType</code> is a placeholder, just the <code>AssocTypeId</code></p>



<a name="194346801"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194346801" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194346801">(Apr 16 2020 at 18:22)</a>:</h4>
<p>Yeah, but <code>TyData::Apply</code> has a substitution in it</p>



<a name="194347484"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194347484" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194347484">(Apr 16 2020 at 18:27)</a>:</h4>
<p>That makes a difference in the generated clauses</p>



<a name="194347591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194347591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194347591">(Apr 16 2020 at 18:28)</a>:</h4>
<p>See <a href="https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses/program_clauses.rs#L590" title="https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses/program_clauses.rs#L590">here</a>:</p>



<a name="194347621"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194347621" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194347621">(Apr 16 2020 at 18:28)</a>:</h4>
<div class="codehilite"><pre><span></span>-- Rule AliasEq-Placeholder
forall&lt;Self, &#39;a, T&gt; {
    AliasEq(&lt;Self as Foo&gt;::Assoc&lt;&#39;a, T&gt; = (Foo::Assoc&lt;&#39;a, T&gt;)&lt;Self&gt;).
 }
</pre></div>



<a name="194347731"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194347731" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194347731">(Apr 16 2020 at 18:29)</a>:</h4>
<p><code>&lt;Self as Foo&gt;::Assoc&lt;'a, T&gt;</code> is the <code>AliasTy</code>, and <code>(Foo::Assoc&lt;'a, T&gt;)&lt;Self&gt;</code> is the <code>TyData::Apply</code></p>



<a name="194347882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194347882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194347882">(Apr 16 2020 at 18:30)</a>:</h4>
<p>I find the syntax distinction here a bit confusing, for opaque types it's more clear that <code>!T</code> is the placeholder and <code>T</code> the actual opaque type</p>



<a name="194348093"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194348093" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194348093">(Apr 16 2020 at 18:32)</a>:</h4>
<p>What's the semantic difference? One of the two is opaque or something?</p>



<a name="194348191"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194348191" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194348191">(Apr 16 2020 at 18:32)</a>:</h4>
<p>Yes, you don't always know the exact type when referring to it</p>



<a name="194354036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194354036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194354036">(Apr 16 2020 at 19:16)</a>:</h4>
<p>I don't get it</p>



<a name="194354685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194354685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194354685">(Apr 16 2020 at 19:21)</a>:</h4>
<p>Nevermind, I think I get it</p>



<a name="194359166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194359166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194359166">(Apr 16 2020 at 19:59)</a>:</h4>
<p>Hmm, I did syn eq for alias types, and the only problem I encountered is (I assume) coinductive check (only <code>cyclic_wf_requirements</code> is not green)</p>



<a name="194367045"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194367045" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194367045">(Apr 16 2020 at 21:01)</a>:</h4>
<p>I pushed a draft implementation</p>



<a name="194422556"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194422556" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194422556">(Apr 17 2020 at 10:44)</a>:</h4>
<p>You can push off reviewing syn-eq pr, if you don't have time, and I'll investigate the coinductive thing myself. I just thought you might have an easy insight</p>



<a name="194446264"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194446264" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194446264">(Apr 17 2020 at 14:15)</a>:</h4>
<p>We'll see, I have a few things to take care of today, I'm not sure how much time i'll get for reviewing</p>



<a name="194446332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194446332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194446332">(Apr 17 2020 at 14:16)</a>:</h4>
<p>but yes please tell me the order <em>you</em> would prefer, that's helpful :)</p>



<a name="194446355"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194446355" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194446355">(Apr 17 2020 at 14:16)</a>:</h4>
<p>Also, I'm not even sure what you mean by "the coinductive thing" (maybe I've not yet seen a GH notification or something)</p>



<a name="194447886"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194447886" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194447886">(Apr 17 2020 at 14:26)</a>:</h4>
<p>So I implemented sem-to-syn for aliases, the only test that is failing is <code>cyclic_wf_requirements</code>:</p>
<div class="codehilite"><pre><span></span>            trait Foo where &lt;Self as Foo&gt;::Value: Foo {
                type Value;
            }

            struct Unit { }
            impl Foo for Unit {
                type Value = Unit;
            }
</pre></div>



<a name="194448030"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194448030" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194448030">(Apr 17 2020 at 14:27)</a>:</h4>
<p>Which, I assume, is about coinductive reasoning for <code>WellFormed</code></p>



<a name="194455569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/194455569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#194455569">(Apr 17 2020 at 15:12)</a>:</h4>
<p>ps <span class="user-mention" data-user-id="251766">@Areredify</span> I branched off the comments you've made on this topic here</p>



<a name="196117824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196117824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196117824">(May 03 2020 at 19:11)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> what are the options to debug the proving process? I can't understand why this isn't provable: </p>
<div class="codehilite"><pre><span></span><code>trait Foo where &lt;Self as Foo&gt;::Value: Foo {
      type Value;
}
struct Unit { }
impl Foo for Unit {
type Value = Unit;
----
clauses:
for&lt;type, type&gt; AliasEq(&lt;^0.0 as Foo&gt;::Value = ^0.1) :- Normalize(&lt;^0.0 as Foo&gt;::Value -&gt; ^0.1),
for&lt;type&gt; WellFormed(^0.0: Foo) :- ForAll&lt;&gt; { Exists&lt;type&gt; { all(WellFormed(^0.0: Foo), AliasEq(&lt;^2.0 as Foo&gt;::Value = ^0.0)) } }, Implemented(^0.0: Foo),
Implemented(Unit: Foo),
Normalize(&lt;Unit as Foo&gt;::Value -&gt; Unit),
(other clauses omitted)
-----
goal {
      WellFormed(Unit: Foo)
}
</code></pre></div>


<p>It should be provable, right? I feel like im going crazy, I've been staring at CHALK_DEBUG=2 for two days now</p>



<a name="196117904"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196117904" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196117904">(May 03 2020 at 19:13)</a>:</h4>
<p>I generally just stare at CHALK_DEBUG=2. let me take a look</p>



<a name="196118185"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196118185" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196118185">(May 03 2020 at 19:20)</a>:</h4>
<p>I pushed latest changes, if you need the code. The test is <code>cyclic_wf_requirements</code></p>



<a name="196118560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196118560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196118560">(May 03 2020 at 19:31)</a>:</h4>
<p>There are several failing tests?</p>



<a name="196118563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196118563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196118563">(May 03 2020 at 19:31)</a>:</h4>
<div class="codehilite"><pre><span></span><code>lowering::assoc_tys
test::coherence::nonoverlapping_assoc_types
test::implied_bounds::implied_from_env
test::projection::gat_unify_with_implied_wc
test::projection::rust_analyzer_regression
test::wf_lowering::cyclic_wf_requirements
</code></pre></div>



<a name="196118578"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196118578" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196118578">(May 03 2020 at 19:31)</a>:</h4>
<p>Yeah that's fine, they should be failing</p>



<a name="196118590"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196118590" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196118590">(May 03 2020 at 19:31)</a>:</h4>
<p>Okay</p>



<a name="196120098"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120098" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120098">(May 03 2020 at 20:00)</a>:</h4>
<p>So, another thing that is helpful is to diff the <code>CHALK_DEBUG</code> log pre vs post PR</p>



<a name="196120567"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120567" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120567">(May 03 2020 at 20:11)</a>:</h4>
<p>do you want me to try it or you already did that?</p>



<a name="196120635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120635">(May 03 2020 at 20:13)</a>:</h4>
<p>I have it</p>



<a name="196120637"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120637" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120637">(May 03 2020 at 20:13)</a>:</h4>
<p><a href="https://www.diffchecker.com/BlBbGNmW" title="https://www.diffchecker.com/BlBbGNmW">https://www.diffchecker.com/BlBbGNmW</a></p>



<a name="196120641"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120641" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120641">(May 03 2020 at 20:13)</a>:</h4>
<p>looking through it</p>



<a name="196120826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120826">(May 03 2020 at 20:17)</a>:</h4>
<p>wow that is helpful</p>



<a name="196120840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196120840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196120840">(May 03 2020 at 20:18)</a>:</h4>
<p>indeed</p>



<a name="196121100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121100">(May 03 2020 at 20:22)</a>:</h4>
<p>Specifically, look at line 4613 in source</p>



<a name="196121204"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121204" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121204">(May 03 2020 at 20:24)</a>:</h4>
<p>Yeah, I noticed that</p>



<a name="196121276"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121276" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121276">(May 03 2020 at 20:26)</a>:</h4>
<p>Specifically,<code>WellFormed</code> goals are coinductive</p>



<a name="196121278"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121278" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121278">(May 03 2020 at 20:26)</a>:</h4>
<p>but, <code>AliasEq</code> is not</p>



<a name="196121292"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121292" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121292">(May 03 2020 at 20:26)</a>:</h4>
<p>Why does it say "no new answers" shortly after? We have  <code>AliasEq(&lt;Unit as Foo&gt;::Value = ?0)</code> which we can prove to get <code>?0</code>, right?</p>



<a name="196121322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121322">(May 03 2020 at 20:27)</a>:</h4>
<p>Because the strand results in a non-coinductive cycle</p>



<a name="196121324"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121324" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121324">(May 03 2020 at 20:27)</a>:</h4>
<p>and is discarded</p>



<a name="196121392"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121392" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121392">(May 03 2020 at 20:28)</a>:</h4>
<p>Non-coinductive cycle meaning there is at least one non-coinductive goal in the cycle to prove?</p>



<a name="196121409"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121409" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121409">(May 03 2020 at 20:29)</a>:</h4>
<p>right</p>



<a name="196121412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121412">(May 03 2020 at 20:29)</a>:</h4>
<p>so</p>



<a name="196121498"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121498" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121498">(May 03 2020 at 20:30)</a>:</h4>
<p>one sec</p>



<a name="196121516"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121516" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121516">(May 03 2020 at 20:31)</a>:</h4>
<p>table 8 has the goal <code>WellFormed(^0.0: Foo)</code></p>



<a name="196121522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121522">(May 03 2020 at 20:31)</a>:</h4>
<p>one of the strands has the subgoals:</p>



<a name="196121527"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121527" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121527">(May 03 2020 at 20:31)</a>:</h4>
<p><code>ForAll&lt;&gt; { Exists&lt;type&gt; { all(WellFormed(^0.0: Foo), AliasEq(&lt;?0 as Foo&gt;::Value = ^0.0)) } }</code></p>



<a name="196121536"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121536" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121536">(May 03 2020 at 20:31)</a>:</h4>
<p>and <code>Implemented(?0: Foo)</code></p>



<a name="196121596"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121596" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121596">(May 03 2020 at 20:32)</a>:</h4>
<p>Aye</p>



<a name="196121622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121622">(May 03 2020 at 20:32)</a>:</h4>
<p>And <code>WellFormed(?0: Foo)</code> is a subgoal for table 7</p>



<a name="196121629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121629">(May 03 2020 at 20:33)</a>:</h4>
<p>which has a goal <code>ForAll&lt;&gt; { Exists&lt;type&gt; { all(WellFormed(^0.0: Foo), AliasEq(&lt;Unit as Foo&gt;::Value = ^0.0)) } }</code></p>



<a name="196121706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121706">(May 03 2020 at 20:34)</a>:</h4>
<p>And <code>ForAll&lt;&gt; { Exists&lt;type&gt; { all(WellFormed(^0.0: Foo), AliasEq(&lt;Unit as Foo&gt;::Value = ^0.0)) } }</code> is a subgoal for table 1</p>



<a name="196121716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121716">(May 03 2020 at 20:34)</a>:</h4>
<p>I think I wrote those down right</p>



<a name="196121720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121720">(May 03 2020 at 20:34)</a>:</h4>
<p>maybe</p>



<a name="196121820"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121820" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121820">(May 03 2020 at 20:37)</a>:</h4>
<p>(side note that I think tracing support will make finding the table stack easier)</p>



<a name="196121838"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196121838" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196121838">(May 03 2020 at 20:37)</a>:</h4>
<p>I certainly hope so</p>



<a name="196122215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196122215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196122215">(May 03 2020 at 20:44)</a>:</h4>
<p>The other tough part of going through the chalk debug output is trying to filter out bits of the program that you've already seen to be proven</p>



<a name="196122471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196122471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196122471">(May 03 2020 at 20:49)</a>:</h4>
<p>Yeah we really need some tool to visualize the process or something, we will inevitably hit a bug with a convoluted set of clauses, it will be a nightmare to debug</p>



<a name="196126274"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126274" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126274">(May 03 2020 at 22:25)</a>:</h4>
<p>So I've been thinking through this a bit</p>



<a name="196126313"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126313" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126313">(May 03 2020 at 22:26)</a>:</h4>
<p>And not really getting very far</p>



<a name="196126315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126315">(May 03 2020 at 22:26)</a>:</h4>
<p>(in regards to what the proper solution is here)</p>



<a name="196126319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126319">(May 03 2020 at 22:26)</a>:</h4>
<p>I'm thinking that the <code>WellFormed</code> goal should <em>not</em> be "lowered"</p>



<a name="196126327"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126327" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126327">(May 03 2020 at 22:27)</a>:</h4>
<p>But I'm not sure if that's the most elegant solution here</p>



<a name="196126386"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126386" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126386">(May 03 2020 at 22:29)</a>:</h4>
<p>We should probably put it on the agenda</p>



<a name="196126389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126389">(May 03 2020 at 22:29)</a>:</h4>
<p>Good idea :)</p>



<a name="196126432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126432">(May 03 2020 at 22:30)</a>:</h4>
<p>The other thing that's potentially weird</p>



<a name="196126438"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126438" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126438">(May 03 2020 at 22:30)</a>:</h4>
<p>I'm trying to gather the info into a coherent post</p>



<a name="196126468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126468">(May 03 2020 at 22:31)</a>:</h4>
<p>But essentially, using a bound var for the new type is causing problems because it get's canonicalized to an inference variable</p>



<a name="196126508"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196126508" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196126508">(May 03 2020 at 22:32)</a>:</h4>
<p>And we lose that we are in a coinductive <code>WellFormed(?0: Foo)</code> cycle</p>



<a name="196233215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233215">(May 04 2020 at 20:05)</a>:</h4>
<p>hmm</p>



<a name="196233482"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233482" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233482">(May 04 2020 at 20:07)</a>:</h4>
<p>Does <code>WellFormed</code> flounder if it's input type is an inference variable?</p>



<a name="196233756"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233756" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233756">(May 04 2020 at 20:09)</a>:</h4>
<p>Mmm, no</p>



<a name="196233809"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233809" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233809">(May 04 2020 at 20:09)</a>:</h4>
<p>I wonder if that would help here</p>



<a name="196233838"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233838" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233838">(May 04 2020 at 20:10)</a>:</h4>
<p>I would think so</p>



<a name="196233888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233888">(May 04 2020 at 20:10)</a>:</h4>
<p>because we want to process the <code>AliasEq</code> first</p>



<a name="196233959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233959">(May 04 2020 at 20:10)</a>:</h4>
<p>Well ... hmm</p>



<a name="196233984"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196233984" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196233984">(May 04 2020 at 20:11)</a>:</h4>
<p>Maybe that would work</p>



<a name="196234435"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196234435" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196234435">(May 04 2020 at 20:14)</a>:</h4>
<p>I'll try that then</p>



<a name="196234899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196234899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196234899">(May 04 2020 at 20:19)</a>:</h4>
<p>The test is still red, assuming I did it correctly</p>



<a name="196234932"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196234932" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196234932">(May 04 2020 at 20:19)</a>:</h4>
<p>It worked for me</p>



<a name="196234997"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196234997" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196234997">(May 04 2020 at 20:20)</a>:</h4>
<p>err wait</p>



<a name="196235001"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235001" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235001">(May 04 2020 at 20:20)</a>:</h4>
<p>I'm on master</p>



<a name="196235015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235015">(May 04 2020 at 20:20)</a>:</h4>
<p><span aria-label="face palm" class="emoji emoji-1f926" role="img" title="face palm">:face_palm:</span>‍♀️</p>



<a name="196235041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235041">(May 04 2020 at 20:20)</a>:</h4>
<div class="codehilite"><pre><span></span><code>DomainGoal::WellFormed(WellFormed::Trait(trait_ref)) =&gt; {
            if trait_ref.self_type_parameter(interner).is_var(interner) {
                return Err(Floundered);
            }
            db.trait_datum(trait_ref.trait_id)
                .to_program_clauses(builder);
        }
</code></pre></div>



<a name="196235447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235447">(May 04 2020 at 20:24)</a>:</h4>
<p>Do we substitute out the inference variable once we find a solution on the other subgoal? I don't remember</p>



<a name="196235485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235485">(May 04 2020 at 20:25)</a>:</h4>
<p>I don't think so</p>



<a name="196235776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196235776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196235776">(May 04 2020 at 20:28)</a>:</h4>
<p>then this should always cause the strand to flounder still</p>



<a name="196237949"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196237949" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196237949">(May 04 2020 at 20:47)</a>:</h4>
<p><span class="user-mention" data-user-id="251766">@Areredify</span> is your PR up to date with the changes from the branch?</p>



<a name="196237979"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196237979" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196237979">(May 04 2020 at 20:47)</a>:</h4>
<p>yes</p>



<a name="196238239"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238239" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238239">(May 04 2020 at 20:49)</a>:</h4>
<p>Note that it doesn't respect internal binders and some other stuff</p>



<a name="196238288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238288">(May 04 2020 at 20:49)</a>:</h4>
<p>IIRC the PR looked incomplete when I last looked at it</p>



<a name="196238409"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238409" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238409">(May 04 2020 at 20:50)</a>:</h4>
<p>I'm trying to remember why :)</p>



<a name="196238419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238419">(May 04 2020 at 20:50)</a>:</h4>
<p>That's because it is :)</p>



<a name="196238425"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238425" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238425">(May 04 2020 at 20:50)</a>:</h4>
<p>for one thing, maybe, it didn't lower goals? (maybe it does now?)</p>



<a name="196238438"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238438" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238438">(May 04 2020 at 20:50)</a>:</h4>
<p>It does now</p>



<a name="196238461"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238461" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238461">(May 04 2020 at 20:51)</a>:</h4>
<p>But it only handles projection aliases</p>



<a name="196238727"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238727" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238727">(May 04 2020 at 20:53)</a>:</h4>
<p>And doesn't respect internal binders</p>



<a name="196238773"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238773" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238773">(May 04 2020 at 20:53)</a>:</h4>
<p>That test was driving me crazy so I didn't finish it <span aria-label="crying cat" class="emoji emoji-1f63f" role="img" title="crying cat">:crying_cat:</span></p>



<a name="196238829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238829">(May 04 2020 at 20:54)</a>:</h4>
<p>which test is it exactly?</p>



<a name="196238840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238840">(May 04 2020 at 20:54)</a>:</h4>
<p>I've got it building locally now</p>



<a name="196238858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238858">(May 04 2020 at 20:54)</a>:</h4>
<p>cyclic_wf_requirements</p>



<a name="196238965"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196238965" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196238965">(May 04 2020 at 20:55)</a>:</h4>
<p>I have pre-lowering/past-lowering clauses saved, if you don't want to generate them yourself</p>



<a name="196239876"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196239876" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196239876">(May 04 2020 at 21:03)</a>:</h4>
<p>so</p>



<a name="196239885"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196239885" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196239885">(May 04 2020 at 21:03)</a>:</h4>
<p>I added in the floundring change and some debug output</p>



<a name="196239888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196239888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196239888">(May 04 2020 at 21:03)</a>:</h4>
<p>and I see this:</p>



<a name="196239893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196239893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196239893">(May 04 2020 at 21:03)</a>:</h4>
<div class="codehilite"><pre><span></span><code>: <span class="o">|</span><span class="w"> </span><span class="n">top_of_stack_is_coinductive_from</span><span class="p">(</span><span class="n">depth</span><span class="o">=</span><span class="n">StackIndex</span><span class="p">(</span><span class="mi">1</span><span class="p">))</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
: : <span class="o">|</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">StackIndex</span><span class="p">(</span><span class="mi">1</span><span class="p">),</span><span class="w"> </span><span class="n">table</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">UCanonical</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">canonical</span>: <span class="nc">Canonical</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">value</span>: <span class="nc">InEnvironment</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">environment</span>: <span class="nc">Env</span><span class="p">([</span><span class="n">FromEnv</span><span class="p">(</span><span class="n">Unit</span><span class="p">)]),</span><span class="w"> </span><span class="n">goal</span>: <span class="nc">WellFormed</span><span class="p">(</span><span class="n">Unit</span>: <span class="nc">Foo</span><span class="p">)</span><span class="w"> </span><span class="p">},</span><span class="w"> </span><span class="n">binders</span>: <span class="p">[]</span><span class="w"> </span><span class="p">},</span><span class="w"> </span><span class="n">universes</span>: <span class="mi">1</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
: : <span class="o">|</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">StackIndex</span><span class="p">(</span><span class="mi">2</span><span class="p">),</span><span class="w"> </span><span class="n">table</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">UCanonical</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">canonical</span>: <span class="nc">Canonical</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">value</span>: <span class="nc">InEnvironment</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">environment</span>: <span class="nc">Env</span><span class="p">([</span><span class="n">FromEnv</span><span class="p">(</span><span class="n">Unit</span><span class="p">)]),</span><span class="w"> </span><span class="n">goal</span>: <span class="nc">ForAll</span><span class="o">&lt;&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">Exists</span><span class="o">&lt;</span><span class="k">type</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">all</span><span class="p">(</span><span class="n">WellFormed</span><span class="p">(</span><span class="o">^</span><span class="mf">0.0</span>: <span class="nc">Foo</span><span class="p">),</span><span class="w"> </span><span class="n">AliasEq</span><span class="p">(</span><span class="o">&lt;</span><span class="n">Unit</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="n">Foo</span><span class="o">&gt;</span>::<span class="n">Value</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">^</span><span class="mf">0.0</span><span class="p">))</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="p">},</span><span class="w"> </span><span class="n">binders</span>: <span class="p">[]</span><span class="w"> </span><span class="p">},</span><span class="w"> </span><span class="n">universes</span>: <span class="mi">1</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
: <span class="o">|</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="196239997"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196239997" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196239997">(May 04 2020 at 21:04)</a>:</h4>
<p>Extracting out the interesting bits, we get this cycle:</p>
<ul>
<li><code>WellFormed(Unit: Foo)</code></li>
<li><code>ForAll&lt;&gt; { Exists&lt;type&gt; { all(WellFormed(^0.0: Foo), AliasEq(&lt;Unit as Foo&gt;::Value = ^0.0)) } } }</code></li>
<li><code>WellFormed(Unit: Foo)</code> &lt;-- this is the thing we are now trying to prove, again</li>
</ul>



<a name="196240025"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240025" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240025">(May 04 2020 at 21:04)</a>:</h4>
<p>I think this is a kind of pre-existing bug that has been exposed in the notion of a coinductive cycle</p>



<a name="196240193"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240193" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240193">(May 04 2020 at 21:06)</a>:</h4>
<p>These combinators, like <code>ForAll</code>, <code>Exists</code>, <code>all</code>... I guess that they should be considered coinductive...probably?</p>



<a name="196240438"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240438" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240438">(May 04 2020 at 21:08)</a>:</h4>
<p>ok, I see we have this logic:</p>
<div class="codehilite"><pre><span></span><code><span class="w">            </span><span class="n">GoalData</span>::<span class="n">Quantified</span><span class="p">(</span><span class="n">QuantifierKind</span>::<span class="n">ForAll</span><span class="p">,</span><span class="w"> </span><span class="n">goal</span><span class="p">)</span><span class="w"> </span><span class="o">=&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">goal</span><span class="p">.</span><span class="n">skip_binders</span><span class="p">().</span><span class="n">is_coinductive</span><span class="p">(</span><span class="n">db</span><span class="p">)</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="196240602"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240602" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240602">(May 04 2020 at 21:10)</a>:</h4>
<p><span class="user-mention" data-user-id="251766">@Areredify</span> so i'm going to push a WIP commit that makes it pass, but I'm not yet sure about all of the changes :)</p>



<a name="196240783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240783">(May 04 2020 at 21:12)</a>:</h4>
<p>I am not qualified to talk about coinductivness, guess I'll have to fill in the blanks</p>



<a name="196240801"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240801" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240801">(May 04 2020 at 21:12)</a>:</h4>
<p>I don't see why those changes would be wrong</p>



<a name="196240837"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240837" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240837">(May 04 2020 at 21:13)</a>:</h4>
<p>Which literature piece is about it? SLG solver paper?</p>



<a name="196240906"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240906" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240906">(May 04 2020 at 21:14)</a>:</h4>
<p>no, the best is probably <a href="https://link.springer.com/chapter/10.1007/11799573_25" title="https://link.springer.com/chapter/10.1007/11799573_25">Coinductive Logic Programming</a>, or better yet Luke Simon's thesis</p>



<a name="196240976"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240976" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240976">(May 04 2020 at 21:14)</a>:</h4>
<p>with those changes I get these errors:</p>



<a name="196240988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196240988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196240988">(May 04 2020 at 21:14)</a>:</h4>
<div class="codehilite"><pre><span></span><code>lowering::assoc_tys
test::coherence::nonoverlapping_assoc_types
test::implied_bounds::implied_from_env
test::projection::gat_unify_with_implied_wc
test::projection::rust_analyzer_regression
</code></pre></div>



<a name="196241002"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241002" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241002">(May 04 2020 at 21:14)</a>:</h4>
<p>That is expected</p>



<a name="196241014"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241014" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241014">(May 04 2020 at 21:15)</a>:</h4>
<p>Thank you, you are a lifesaver</p>



<a name="196241058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241058">(May 04 2020 at 21:15)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364/near/196240906" title="#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364/near/196240906">said</a>:</p>
<blockquote>
<p>no, the best is probably <a href="https://link.springer.com/chapter/10.1007/11799573_25" title="https://link.springer.com/chapter/10.1007/11799573_25">Coinductive Logic Programming</a>, or better yet Luke Simon's thesis</p>
</blockquote>
<p>Do I need to read both or the thesis would be sufficient?</p>



<a name="196241079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241079">(May 04 2020 at 21:15)</a>:</h4>
<p>the thesis suffices, it's just an expanded version of that paper</p>



<a name="196241222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241222">(May 04 2020 at 21:17)</a>:</h4>
<p>I'll at least push an expanded comment with my reasoning</p>



<a name="196241840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241840">(May 04 2020 at 21:23)</a>:</h4>
<p>done</p>



<a name="196241937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241937">(May 04 2020 at 21:24)</a>:</h4>
<p>pretty much convinced myself that <code>ForAll</code>, <code>Exists</code>, and <code>All</code> could all be considered coinductive all the time and it would be fine.</p>



<a name="196241961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196241961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196241961">(May 04 2020 at 21:24)</a>:</h4>
<p>I need convincing</p>



<a name="196242008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242008">(May 04 2020 at 21:25)</a>:</h4>
<p>Consider this comment:</p>
<div class="codehilite"><pre><span></span><code>            // The &quot;All(...)&quot; quantifier is considered coinductive. This could
            // be somewhat surprising as you might have `All(Gc, Gi)` where `Gc`
            // is coinductive and `Gi` is inductive. This however is really no
            // different than defining a fresh coinductive goal like
            //
            // ```notrust
            // Gx :- Gc, Gi
            // ```
            //
            // and requiring `Gx` in place of `All(Gc, Gi)`, and that would be
            // perfectly reasonable.
</code></pre></div>



<a name="196242131"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242131" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242131">(May 04 2020 at 21:26)</a>:</h4>
<p>but in a more operational vein, if you ever have a cycle that involves an inductive participant, it will .. well .. show up in the cycle.</p>



<a name="196242149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242149">(May 04 2020 at 21:26)</a>:</h4>
<p>i.e., if you had <code>Gi :- Gx</code>, in that example above, it would not be provable</p>



<a name="196242289"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242289" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242289">(May 04 2020 at 21:28)</a>:</h4>
<p>Hmm</p>



<a name="196242694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242694">(May 04 2020 at 21:33)</a>:</h4>
<p>So</p>



<a name="196242725"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242725" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242725">(May 04 2020 at 21:33)</a>:</h4>
<p>I don't think think <code>All(Gc, Gi)</code> being coinductive is the same as <code>Gx</code> being coinductive</p>



<a name="196242828"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242828" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242828">(May 04 2020 at 21:34)</a>:</h4>
<p>I'm trying to put this into words and convince myself one way or the other</p>



<a name="196242845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242845">(May 04 2020 at 21:34)</a>:</h4>
<p>specifically, I'm trying to think of a counter example</p>



<a name="196242850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242850">(May 04 2020 at 21:34)</a>:</h4>
<p>Is <code>All(Gi)</code> coinductive, but <code>Gi</code> is not?</p>



<a name="196242899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196242899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196242899">(May 04 2020 at 21:35)</a>:</h4>
<p>That is really surprising</p>



<a name="196243052"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243052" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243052">(May 04 2020 at 21:36)</a>:</h4>
<p>It is surprising, but I think it is correct.</p>



<a name="196243116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243116">(May 04 2020 at 21:37)</a>:</h4>
<p>Is <code>All(Gi) :- All(Gi)</code> a trivial cycle?</p>



<a name="196243129"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243129" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243129">(May 04 2020 at 21:37)</a>:</h4>
<p>i.e,. I don't think it allows you to prove anything surprising :)</p>



<a name="196243138"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243138" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243138">(May 04 2020 at 21:37)</a>:</h4>
<p>Sure, if you have this rule, but we don't</p>



<a name="196243153"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243153" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243153">(May 04 2020 at 21:37)</a>:</h4>
<p>That rule would be wrong regardless</p>



<a name="196243164"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243164" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243164">(May 04 2020 at 21:37)</a>:</h4>
<p>like, it wouldn't capture the semantics of "all" that we expect</p>



<a name="196243223"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243223" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243223">(May 04 2020 at 21:38)</a>:</h4>
<p>Oh <code>all</code> is not a domain goal</p>



<a name="196243227"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243227" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243227">(May 04 2020 at 21:38)</a>:</h4>
<p>right</p>



<a name="196243239"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243239" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243239">(May 04 2020 at 21:38)</a>:</h4>
<p>it's built-in to the solver</p>



<a name="196243292"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243292" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243292">(May 04 2020 at 21:39)</a>:</h4>
<p>in fact, in some sense, the fact that it's on the stack <em>at all</em> is an impl artifact I think</p>



<a name="196243420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243420">(May 04 2020 at 21:40)</a>:</h4>
<p>Hmm?</p>



<a name="196243676"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243676" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243676">(May 04 2020 at 21:42)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364/near/196243292" title="#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364/near/196243292">said</a>:</p>
<blockquote>
<p>in fact, in some sense, the fact that it's on the stack <em>at all</em> is an impl artifact I think</p>
</blockquote>
<p>I think <em>this</em> is more of the "correct" solution here</p>



<a name="196243707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243707">(May 04 2020 at 21:43)</a>:</h4>
<p>well, removing that artifact, that is</p>



<a name="196243717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243717">(May 04 2020 at 21:43)</a>:</h4>
<p>If that's possible</p>



<a name="196243738"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243738" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243738">(May 04 2020 at 21:43)</a>:</h4>
<p>I...don't <em>dis</em>agree, but I also don't fully <em>agree</em></p>



<a name="196243794"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243794" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243794">(May 04 2020 at 21:44)</a>:</h4>
<p>yeah, I'm thinking about what I just said</p>



<a name="196243795"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243795" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243795">(May 04 2020 at 21:44)</a>:</h4>
<p>that is, I agree it's more "correct" but I'm not sure it's what we want to do</p>



<a name="196243799"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243799" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243799">(May 04 2020 at 21:44)</a>:</h4>
<p>and considering if I regret it</p>



<a name="196243812"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243812" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243812">(May 04 2020 at 21:44)</a>:</h4>
<p>I'm very sure it's not what we want to do <em>right now</em></p>



<a name="196243886"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243886" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243886">(May 04 2020 at 21:45)</a>:</h4>
<p>I think I agree with you that <code>All</code> is coinductive</p>



<a name="196243893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/196243893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#196243893">(May 04 2020 at 21:45)</a>:</h4>
<p>I think that this "Gx" rule is pretty convincing -- if it makes any sense to combine inductive and coinductive predicates, then the <code>Gx</code> example ought to be valid and prove what one expects (i.e., it holds if <code>Gi</code> and <code>Gc</code> are true, etc)</p>



<a name="197337457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/197337457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#197337457">(May 12 2020 at 20:51)</a>:</h4>
<p>Hm, so I'll work on this after finishing the generic arg work</p>



<a name="197337568"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/197337568" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#197337568">(May 12 2020 at 20:51)</a>:</h4>
<p>yeah, seems good</p>



<a name="213473720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213473720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213473720">(Oct 15 2020 at 19:11)</a>:</h4>
<p>Okay, reviving this a little bit. (Now PR <a href="https://github.com/rust-lang/rust/issues/589">#589</a>)</p>



<a name="213473735"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213473735" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213473735">(Oct 15 2020 at 19:11)</a>:</h4>
<p>I looked at this a bit</p>



<a name="213473743"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213473743" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213473743">(Oct 15 2020 at 19:11)</a>:</h4>
<p><span class="user-mention" data-user-id="230601">@Nathan Whitaker</span></p>



<a name="213473816"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213473816" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213473816">(Oct 15 2020 at 19:11)</a>:</h4>
<p>So, you have in a comment that:</p>
<div class="codehilite" data-code-language="notrust"><pre><span></span><code> forall&lt;X&gt; {
     Implemented(&lt;X as Iterator&gt;::Item&gt;: Debug) :-
         Implemented(X: Debug)
 }
</code></pre></div>

<p>would lower this into:</p>
<div class="codehilite" data-code-language="notrust"><pre><span></span><code> forall&lt;X, Y&gt; {
     Implemented(Y: Debug) :-
         AliasEq(&lt;X as Iterator&gt;::Item&gt;, Y),
         Implemented(X: Debug)
 }
</code></pre></div>



<a name="213473831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213473831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213473831">(Oct 15 2020 at 19:11)</a>:</h4>
<p>oh that is ugly..</p>



<a name="213474022"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474022" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474022">(Oct 15 2020 at 19:13)</a>:</h4>
<p>okay better</p>



<a name="213474028"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474028" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474028">(Oct 15 2020 at 19:13)</a>:</h4>
<p>anyways, that looks right</p>



<a name="213474036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474036">(Oct 15 2020 at 19:13)</a>:</h4>
<p>But, the code actually doesn't do that</p>



<a name="213474075"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474075" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474075">(Oct 15 2020 at 19:13)</a>:</h4>
<p>Instead of an <code>AliasEq</code>, it actually lowers into an <code>EqGoal</code></p>



<a name="213474144"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474144" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474144">(Oct 15 2020 at 19:14)</a>:</h4>
<p>I changed it to <code>AliasEq</code> locally and only two tests fail!</p>



<a name="213474478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474478">(Oct 15 2020 at 19:16)</a>:</h4>
<p>(implied_bounds::implied_from_env and projection::gat_unify_with_implied_wc)</p>



<a name="213474514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213474514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213474514">(Oct 15 2020 at 19:17)</a>:</h4>
<p>Didn't get to look much into exactly why yet, but something we should discuss</p>



<a name="213476373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213476373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213476373">(Oct 15 2020 at 19:31)</a>:</h4>
<p>Ah right I forgot about that. So when I wrote that comment we <em>were</em> emitting an <code>AliasEq</code> instead, but as you noticed it caused some test failures.</p>



<a name="213476867"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213476867" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213476867">(Oct 15 2020 at 19:35)</a>:</h4>
<p>The reason is that our current environment elaboration isn't super smart. Basically it visits the program clauses currently in the env and in doing so it only <a href="https://github.com/rust-lang/chalk/blob/d7c75db36d4c08f283a8ead2160efe3e9542ea32/chalk-solve/src/clauses/env_elaborator.rs#L85">recursively visits <code>FromEnv</code> domain goals</a>.</p>



<a name="213476963"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213476963" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213476963">(Oct 15 2020 at 19:36)</a>:</h4>
<p>So my initial fix was to change the elaborator to also recurse on <code>AliasEq</code> domain goals, which seemed non-ideal</p>



<a name="213477189"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213477189" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213477189">(Oct 15 2020 at 19:38)</a>:</h4>
<p>Then as I added the lowering for function types as well, I wanted to clean up the lowering code and so I tried emitting an <code>EqGoal</code> for both , because it eventually becomes an <code>AliasEq</code> goal anyway, and realized that also fixed the issue because <code>EqGoal</code> is a top level goal and so the elaborator recurses into it already.</p>



<a name="213477294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213477294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213477294">(Oct 15 2020 at 19:39)</a>:</h4>
<p>So I figured I'd kill two birds with one stone (cleaning up lowering + fixing the tests) and emit the <code>EqGoal</code>, while not having to change the elaboration code</p>



<a name="213477380"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213477380" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213477380">(Oct 15 2020 at 19:40)</a>:</h4>
<p>TLDR: It's intentional, I just forgot to update the comment</p>



<a name="213477643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213477643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213477643">(Oct 15 2020 at 19:42)</a>:</h4>
<p>huh, yeah I forgot that <code>EqGoal</code> does just end up pushing an <code>AliasEq</code> goal</p>



<a name="213477776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213477776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213477776">(Oct 15 2020 at 19:43)</a>:</h4>
<p>Sounds like the elaboration maybe does need cleanup though</p>



<a name="213517504"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213517504" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213517504">(Oct 16 2020 at 04:20)</a>:</h4>
<p>uh... <a href="https://github.com/rust-lang/chalk/blob/d7c75db36d4c08f283a8ead2160efe3e9542ea32/tests/lowering/mod.rs#L147">https://github.com/rust-lang/chalk/blob/d7c75db36d4c08f283a8ead2160efe3e9542ea32/tests/lowering/mod.rs#L147</a></p>



<a name="213517508"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213517508" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213517508">(Oct 16 2020 at 04:20)</a>:</h4>
<p>That's not valid, right?</p>



<a name="213517513"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213517513" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213517513">(Oct 16 2020 at 04:20)</a>:</h4>
<p>Like, you can't impl a trait for an associated type?</p>



<a name="213520863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213520863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213520863">(Oct 16 2020 at 05:40)</a>:</h4>
<p>Hmm well you can impl a trait for the associated type of a concrete type, but not a generic type (at least currently)</p>



<a name="213520879"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213520879" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Whitaker <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213520879">(Oct 16 2020 at 05:41)</a>:</h4>
<p>But I'm not sure if we eventually want to accept that or not <span aria-label="thinking" class="emoji emoji-1f914" role="img" title="thinking">:thinking:</span></p>



<a name="213524445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/sem-vs-syn-eq%20chalk%23364/near/213524445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthew Jasper <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/sem-vs-syn-eq.20chalk.23364.html#213524445">(Oct 16 2020 at 07:01)</a>:</h4>
<p>That impl is not allowed (X is unconstrained), but this is allowed</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{}</span><span class="w"></span>

<span class="k">impl</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="o">&lt;</span><span class="n">X</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nb">Iterator</span><span class="o">&gt;</span>::<span class="n">Item</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="n">X</span>: <span class="nb">Iterator</span> <span class="p">{}</span><span class="w"></span>
</code></pre></div>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>